$\forall$$A$, $B$:Type, $a$:EqDecider($A$), $b$:EqDecider($B$). proddeq($a$;$b$) $\in$ $A$$\times$$B$$\rightarrow$$A$$\times$$B$$\rightarrow\mathbb{B}$